Інформатика

Мотивація

Важливим етапом в розвитку викладача є не тільки програма для вищої школи четвертого рівня акредитації, але і для середньої школи, а значить кожного учня в кожному селі. Для цих потреб за основу я хочу взяти програму "Інформатика" Манфреда Броя.

Власне, оскільки школа починається з 5 років приблизно, то цей курс у вигляді монографії повинен відповідати вимогам ELI5, шоб кожен вчитель міг відтворити цей курс.

Структура курсу Манфреда Броя

Шо гарного я можу сказати про цю програму: 1) це фулстек програма, яка покриває розробку мовних засобів, дискретну математику і паралельне програмування 2) програма викладається штучно створеною педагогічною мовою для цього типу паскаля 3) логіку починає з Арістотеля.

Чотири теми мого курсу Інформатика наслідують розділ на чотири книги Манфреда Броя і мають наступну структуру:

1) Основи: інформація, алгоритми і структури, мови, їх класи, типи, рекурсія:
    — Інформація, інформаційна система та її властивості.
    — Позиційні системи числення, кодування інформації.
    — Алгоритми, системи переписування термів, ג-числення, рекурсивні функції.
    — Типи і структури даних, Бом дерева, структурна рекурсія.
    — Логіка висловлювань, логіка предикатів, вищі логіки.
    — Мови програмування, граматики, БНФ, лексичний аналіз.
2) Дискретна математика, схемотехніка, асемблери;
    — Булева алгебра та редукція термів. ДНФ, КНФ.
    — Регістри, Лічильники, Логіка, Арифметика.
    — Архітектура компʼютера. SMP, AMP.
    — Узгоджена паралельна обробка черг.
3) Операційні системи, компілятори, рантайми;
    — Числення процесів. Моделі процесів. Мережі Петрі, FSM автомати, BPMN.
    — Операційні системи і рантайми. Реактори, Процеси, Канали, Курсори.
    — Мови. Лексика, Синтаксис. LL, LR, LALR. Інтерпретатори, Компілятори.
4) Формальні мови, обчислювальність, складність, ефективність.
    — Формальні мови. Основи математики.
    — Обчислювальність. Коректність. Складність. Ефективність.
    — Семантика мов програмування. Формальні моделі.
    — Мова опису математики.

Інформація, алгоритми і структури даних, мови, типи, рекурсія.

Дискретна математика і схемотехніка.

Операційні системи, рантайми, інтерпретатори і компілятори.

Формальні мови, обчислювальність, коректність, слкадність, ефективність.

Компілятор мови ML Робіна Мілнера

Оскільки четверта тема є добре пропрацьованою в курсі "Формальна математика", а операційна система з третьої теми теж частина цієї монографії, то найскладніша і націкавіша теми, з якої хочеться почати --- це "Компілятор", який є частиною третьої теми курсу.

Я провів в дослідженні компіляторів, мов програмування і операційних систем 20 років, починаючи від embedded систем TRON, QNX, BeOS до дизасемблювання NT в Soft-ICE і хочу сказати шо ті школи які взяли у якості основи серію мов Standard ML мають неабияку перевагу. Я провів свою юність з мовами серії ML лише поверхово (написали веб-сокет сервер, портували на SML N2O та NITRO), але вже тоді схопив найголовніше: мова ML це єдина промислова мова рівня System F з доведеною семантикою і теоремами про коректність (soundness) написаними в Twelf, головна заслуга тут Роберта Харпера. Мова програмування Standard ML була придумана Робіном Мілнером за яку він дістав премію Тюрінга, один з небагатьох хто заслужено.

Тому замість Pascal/Ada-подібної мови Манфреда Броя, на якій наводяться приклади алгоритмів з його курсу "Інформатика" в нашому курсі ми пропонуємо використовувати ML мову MinCaml розроблену Ейдзіро Суміі в Університеті Токіо.